w{-}action{-}dec(${\it TA}$;$M$;$i$)($k$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$kindcase($k$; $a$.${\it TA}$($i$,$a$); $l$,${\it tg}$.if destination($l$) = $i$$\rightarrow$ $M$($l$,${\it tg}$) else Void fi )